00100	FOL Project 2 Feb 1974
00200	
00300	TASK DESCRIPTION #2
00400	
00500	MISCELLANEOUS IMPROVEMENTS
00600	
00700	
00800		This is  a list of proposed improvements to FOL.  They
00900	are all straightforward to implement and should make a substantial
01000	reduction in the length of proofs when taken together.
01100	
01200		1. Introduce ∃!
01300	∃!x y z.A asserts the existence of unique x, y and z satisfying A.
01400	It is proved by proving ∃x y z.A and ∀x1 x2 y1 y2 z1 z2.(
01500	A(x1z1) ∧ A(x2,y2,z2) ⊃ x1=x2 ∧ y1=y2 ∧ z1=z2).  Its consequences
01600	are the same.  Normally, it will be used in axioms.